(declare-fun b () Int)
(declare-fun o (Int Int) Int)
(declare-fun a () Int)
(declare-fun p () Int)
(declare-fun d () Int)
(declare-fun c () Int)
(declare-fun htrue () Int)
(declare-fun typeof (Int) Int)
(declare-fun owner_43528 () Int)
(declare-fun e () Int)
(declare-fun r () Int)
(declare-fun g () Int)
(declare-fun aitcaa () Int)
(declare-fun ab (Int Int) Int)
(declare-fun h () Int)
(declare-fun ac () Int)
(declare-fun q (Int Int) Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun at (Int Int) Bool)
(assert (at aitcaa c))
(assert (forall ((f Int) (k Int) (l Int)) (= htrue (ab (o (q f k) l) k))))
(assert (forall ((l Int) (k Int)) (= (at k c) (= (= htrue (ab l k)) (or (= l ac) (at (typeof l) k))))))
(assert (forall ((k Int)) (at 0 i)))
(assert (forall ((k Int)) (= (at k a) (= k a))))
(assert (forall ((k Int)) (= (at k d) (= k d))))
(assert (forall ((k Int)) (=> (at k g) (= k g))))
(assert (forall ((k Int)) (=> (at k e) (= k e))))
(assert (forall ((ad Int) (m Int)) (= (at ad ad) (= ad m))))
(assert (forall ((ad Int) (m Int) (n Int)) (= (and (at ad m)) (at ad n))))
(assert (let ((af (= htrue (ab b aitcaa)))(ah (= h j))) (let ((ak (= ah (>= 0 r)))) (not (= true (=> (= owner_43528 (q owner_43528 c)) (not (and (forall ((ao Int)) (= (= htrue (ab ao aitcaa)) (= (o owner_43528 0) ao))) (forall ((ar Int)) (=> (not (= ar ac)) (= (typeof (o p ar)) 0))) (or af ak)))))))))
(check-sat)
